<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>TypeConversionRule</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="TypeConversionRule";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/SubstMapEntry.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/VerifyProofs.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/TypeConversionRule.html" target="_top">Frames</a></li>
<li><a href="TypeConversionRule.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.verify</div>
<h2 title="Class TypeConversionRule" class="title">Class TypeConversionRule</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">mmj.verify.GrammarRule</a></li>
<li>
<ul class="inheritance">
<li>mmj.verify.TypeConversionRule</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">TypeConversionRule</span>
extends <a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></pre>
<div class="block">A Type Conversion Rule is a Grammar Rules that says that any grammatical
 expression of a certain type may be substituted for any expression of another
 grammatical Type.
 <p>
 In Metamath terms, a Type Conversion can be derived from a <code>$a</code>
 statement whose Formula has length equal to 2 and whose 2nd symbol has a
 grammatical Type Code that differs from the 1st Symbol (the first symbol of
 every Metamath Formula must be -- is always -- a Constant, and is, in effect
 a "Type Code").
 <p>
 The most famous Metamath Type Conversion is "cv", from set.mm:
 <code>cv $a class x $.</code>, which states that every set is a class, that any
 set variable or expression with Type "set" can be used as a replacement for
 any class variable or expression with Type "class".)
 <p>
 Type Conversion Rules can also be derived from other Grammar Rules, including
 Type Conversion Rules and Notation Rules. Things get complicated very
 quickly, especially when Nulls Permitted Rules are involved.
 <p>
 An example:
 <p>
 <ul>
 <li><code>$c NUMBER INTEGER POSITIVEINTEGER wff term = $.</code>
 <li><code>$v x y i j m n$.</code>
 <li><code>Nx $f NUMBER x $.</code>
 <li><code>Ny $f NUMBER y $.</code>
 <li><code>Ii $f INTEGER i $.</code>
 <li><code>Ij $f INTEGER j $.</code>
 <li><code>Pm $f POSITIVEINTEGER m $.</code>
 <li><code>Pn $f POSITIVEINTEGER n $.</code>
 <li><code>NullOkPOSITIVEINTEGER $a POSITIVEINTEGER $.</code>
 <li><code>ConvINTEGER $a NUMBER i $.</code>
 <li><code>ConvPOSITIVEINTEGER $a INTEGER m $.</code>
 <li><code>TermAdd $a term m n $.</code>
 <li><code>WffEquals $a wff x = y $.
 </ul>
 <p>
 OK, that very hypothetical example explicitly says that we have:
 <ul>
 <li>Type Code "NUMBER" with variables x and y, and variable hypotheses Nx and
 Ny;
 <li>Type Code "INTEGER" with variables i and j, and variable hypotheses Ii
 and Ij;
 <li>Type Code "POSITIVEINTEGER" with variables m and n, and variable
 hypotheses Pm and Pn.
 <li>Nulls Permitted Rule "NullOkPOSITIVEINTEGER";
 <li>Type Conversion Rules "ConvINTEGER", from Integer to Number, and
 ConvPOSITIVEINTEGER from Positive Integer to Integer;
 <li>Notation Rules "TermAdd" (with Type Code "term") and "WffEquals" (with
 Type Code "wff).
 </ul>
 <p>
 But we're not done yet, those are only the explicit Grammar Rules. A number
 of implicit -- derived -- Grammar Rules follow:
 <p>
 <ul>
 <li>Derived Type Conversion Rule from POSITIVEINTEGER to NUMBER;
 <li>Derived Nulls Permitted Rules for INTEGER, NUMBER, and Term;
 <li>Derived Notation Rules based on TermAdd for expressions "m n", "x y",
 "m i", "m x", "i m", "x m", "i x", and "x i";
 <li>Derived Notation Rules based on WffEquals for expressions "m = n", "m =",
 "= m", "i = j", "i =", "= i", "m = i", "m = x", "i = m", "x = m", "x =" and
 "= x".
 </ul>
 <p>
 <b>WHEW!</b>
 <p>
 Part of mmj's grammar validation checks for Type Conversion loops, such as
 "a ISA b" + "b ISA c" + "c ISA a". It also rejects "a ISA a".
 <p>
 Implicit grammar rules are derived in mmj and made explicit, so if "a ISA b"
 and "z ISA a", then mmj will derive "z ISA b".
 <p>
 Since derived grammar rules may duplicate user-input Syntax Axioms (the
 "base" Grammar Rules), mmj reports as an error a user-input rule that
 duplicates a derived rule already in existence. This means that the user
 should move her rule towards the beginning of the .mm file to establish
 precedence.
 <p>
 In other words, mmj reports as an error any user-input grammar rules that
 have no effect, but silently ignores any newly derived rules that duplicate
 user-input rules (unless there is a Type Code conflict between the two!)</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../CreatingGrammarRulesFromSyntaxAxioms.html">
      CreatingGrammarRulesFromSyntaxAxioms.html</a>, 
<a href="../../ConsolidatedListOfGrammarValidations.html">
      ConsolidatedListOfGrammarValidations.html</a>, 
<a href="../../BasicsOfSyntaxAxiomsAndTypes.html">
      BasicsOfSyntaxAxiomsAndTypes.html</a>, 
<a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#convTyp">convTyp</a></strong></code>
<div class="block">convTyp is the "from" or source Typ Cd for The Type Conversion Rule,
 which is converted "to" the Rule's Type Code.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.verify.GrammarRule">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.verify.<a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></h3>
<code><a href="../../mmj/verify/GrammarRule.html#isBaseRule">isBaseRule</a>, <a href="../../mmj/verify/GrammarRule.html#MAX_SEQ_NBR">MAX_SEQ_NBR</a>, <a href="../../mmj/verify/GrammarRule.html#maxSeqNbr">maxSeqNbr</a>, <a href="../../mmj/verify/GrammarRule.html#nbrHypParamsUsed">nbrHypParamsUsed</a>, <a href="../../mmj/verify/GrammarRule.html#paramTransformationTree">paramTransformationTree</a>, <a href="../../mmj/verify/GrammarRule.html#paramVarHypNode">paramVarHypNode</a>, <a href="../../mmj/verify/GrammarRule.html#RULE_NBR">RULE_NBR</a>, <a href="../../mmj/verify/GrammarRule.html#ruleFormatExpr">ruleFormatExpr</a>, <a href="../../mmj/verify/GrammarRule.html#ruleHypPos">ruleHypPos</a>, <a href="../../mmj/verify/GrammarRule.html#ruleNbr">ruleNbr</a></code></li>
</ul>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#TypeConversionRule()">TypeConversionRule</a></strong>()</code>
<div class="block">Default constructor.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#TypeConversionRule(mmj.verify.Grammar, mmj.lang.Axiom, mmj.lang.Cnst)">TypeConversionRule</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                  <a href="../../mmj/lang/Axiom.html" title="class in mmj.lang">Axiom</a>&nbsp;baseSyntaxAxiom,
                  <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;convTyp)</code>
<div class="block">Constructor -- default GrammarRule for base Syntax Axioms, which means no
 parameter "transformations".</div>
</td>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#TypeConversionRule(mmj.verify.Grammar, mmj.verify.NotationRule, int, mmj.verify.NullsPermittedRule)">TypeConversionRule</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                  <a href="../../mmj/verify/NotationRule.html" title="class in mmj.verify">NotationRule</a>&nbsp;oldNotationRule,
                  int&nbsp;matchIndex,
                  <a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify">NullsPermittedRule</a>&nbsp;nullsPermittedRule)</code>
<div class="block">Builds a new TypeConversionRule using a Notation rule which is being
 "cloned" and modified by substituting the paramTransformationTree from a
 NullsPermittedRule for one of the existing rule's variable hypothesis
 paramTransformationTree nodes.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#TypeConversionRule(mmj.verify.Grammar, mmj.verify.TypeConversionRule, int, mmj.verify.TypeConversionRule)">TypeConversionRule</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                  <a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;oldTCRule,
                  int&nbsp;matchIndex,
                  <a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;typeConversionRule)</code>
<div class="block">Builds a new TypeConversionRule using an existing TypeConversion rule
 which is being "cloned" and and modified by substituting the
 paramTransformationTree from another TypeConversionRule for one of the
 existing rule's variable hypothesis paramTransformationTree nodes.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#addToGrammar(mmj.verify.Grammar, mmj.lang.Cnst[])">addToGrammar</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
            <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]&nbsp;ruleFormatExprIn)</code>
<div class="block">Add Type Conversion rule format expression to the system "repository".</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected static <a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#buildBaseRule(mmj.verify.Grammar, mmj.lang.Axiom, mmj.lang.ParseNodeHolder[])">buildBaseRule</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
             <a href="../../mmj/lang/Axiom.html" title="class in mmj.lang">Axiom</a>&nbsp;baseSyntaxAxiom,
             <a href="../../mmj/lang/ParseNodeHolder.html" title="class in mmj.lang">ParseNodeHolder</a>[]&nbsp;parseNodeHolderExpr)</code>
<div class="block">Type Conversion Rule builder for base Syntax Axioms, which means no
 parameter "transformations".</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#deriveAdditionalRules(mmj.verify.Grammar)">deriveAdditionalRules</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar)</code>
<div class="block">deriveAdditionalRules based on the addition of a new GrammarRule to those
 already generated and accepted.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#deriveRulesUsingNullsPermitted(mmj.verify.Grammar, mmj.verify.NullsPermittedRule)">deriveRulesUsingNullsPermitted</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                              <a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify">NullsPermittedRule</a>&nbsp;nullsPermittedRule)</code>
<div class="block">Generates a NullsPermittedRule *if* the input NullsPermittedRule Type
 Code matches the Type Code of the TypeConversionRule's VarHyp.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#deriveRulesUsingTypeConversion(mmj.verify.Grammar, mmj.verify.TypeConversionRule)">deriveRulesUsingTypeConversion</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                              <a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;typeConversionRule)</code>
<div class="block">Generates a TypeConversionRule *if* the input TypeConversionRule Type
 Code matches the Type Code of this TypeConversionRule's VarHyp.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#getConvTyp()">getConvTyp</a></strong>()</code>
<div class="block">Return convTyp, the "from" part of the Type conversion.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#getDupRule(mmj.verify.Grammar, mmj.lang.Cnst[])">getDupRule</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
          <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]&nbsp;ruleFormatExprIn)</code>
<div class="block">Return a duplicate of the input ruleFormatExpr if it exists, or return
 null.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#getForestRuleExpr()">getForestRuleExpr</a></strong>()</code>
<div class="block">Returns the ruleFormatExpr for the Type Conversion Rule by simulating
 retrieving it from the Grammar Rule Tree/Forest.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/TypeConversionRule.html#isLoop(mmj.lang.Cnst, mmj.lang.Cnst)">isLoop</a></strong>(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;fromTyp,
      <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;toTyp)</code>
<div class="block">isLoop determines whether or not a new Type Conversion from/to pair of
 Type Codes create a "loop" -- meaning that "from" converts to "to" and
 "to" converts to "from", directly or indirectly.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.verify.GrammarRule">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.verify.<a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></h3>
<code><a href="../../mmj/verify/GrammarRule.html#add(mmj.lang.Axiom, mmj.verify.Grammar)">add</a>, <a href="../../mmj/verify/GrammarRule.html#buildGrammaticalParseNode(mmj.lang.ParseNodeHolder[])">buildGrammaticalParseNode</a>, <a href="../../mmj/verify/GrammarRule.html#buildRuleFormatExpr()">buildRuleFormatExpr</a>, <a href="../../mmj/verify/GrammarRule.html#compareTo(java.lang.Object)">compareTo</a>, <a href="../../mmj/verify/GrammarRule.html#equals(java.lang.Object)">equals</a>, <a href="../../mmj/verify/GrammarRule.html#findMatchingVarHypTyp(int, mmj.lang.Cnst)">findMatchingVarHypTyp</a>, <a href="../../mmj/verify/GrammarRule.html#getBaseSyntaxAxiom()">getBaseSyntaxAxiom</a>, <a href="../../mmj/verify/GrammarRule.html#getGrammarRuleTyp()">getGrammarRuleTyp</a>, <a href="../../mmj/verify/GrammarRule.html#getIsBaseRule()">getIsBaseRule</a>, <a href="../../mmj/verify/GrammarRule.html#getMaxSeqNbr()">getMaxSeqNbr</a>, <a href="../../mmj/verify/GrammarRule.html#getNbrHypParamsUsed()">getNbrHypParamsUsed</a>, <a href="../../mmj/verify/GrammarRule.html#getParamTransformationTree()">getParamTransformationTree</a>, <a href="../../mmj/verify/GrammarRule.html#getParamVarHypNode()">getParamVarHypNode</a>, <a href="../../mmj/verify/GrammarRule.html#getParseNodeHolderExpr()">getParseNodeHolderExpr</a>, <a href="../../mmj/verify/GrammarRule.html#getRuleFormatExpr()">getRuleFormatExpr</a>, <a href="../../mmj/verify/GrammarRule.html#getRuleFormatExprAsString()">getRuleFormatExprAsString</a>, <a href="../../mmj/verify/GrammarRule.html#getRuleFormatExprFirst()">getRuleFormatExprFirst</a>, <a href="../../mmj/verify/GrammarRule.html#getRuleFormatExprIthSymbol(int)">getRuleFormatExprIthSymbol</a>, <a href="../../mmj/verify/GrammarRule.html#getRuleHypPos()">getRuleHypPos</a>, <a href="../../mmj/verify/GrammarRule.html#getRuleNbr()">getRuleNbr</a>, <a href="../../mmj/verify/GrammarRule.html#getSyntaxAxiomVarHypReseq()">getSyntaxAxiomVarHypReseq</a>, <a href="../../mmj/verify/GrammarRule.html#hashCode()">hashCode</a>, <a href="../../mmj/verify/GrammarRule.html#setIsBaseRule(boolean)">setIsBaseRule</a>, <a href="../../mmj/verify/GrammarRule.html#setMaxSeqNbr(int)">setMaxSeqNbr</a>, <a href="../../mmj/verify/GrammarRule.html#setNbrHypParamsUsed(int)">setNbrHypParamsUsed</a>, <a href="../../mmj/verify/GrammarRule.html#setRuleFormatExpr(mmj.lang.Cnst[])">setRuleFormatExpr</a>, <a href="../../mmj/verify/GrammarRule.html#showRuleFormatExprAsString(mmj.lang.Cnst[])">showRuleFormatExprAsString</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="convTyp">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>convTyp</h4>
<pre>protected&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a> convTyp</pre>
<div class="block">convTyp is the "from" or source Typ Cd for The Type Conversion Rule,
 which is converted "to" the Rule's Type Code.
 <p>
 Note that there is no need to store the "to" Type code here in the
 TypeConversionRule because it can easily be derived from the Type Code
 via GrammarRule.getBaseSyntaxAxiom().getTyp() AND from the root node's
 Stmt of GrammarRule.paramTransformationTree.</div>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="TypeConversionRule()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>TypeConversionRule</h4>
<pre>public&nbsp;TypeConversionRule()</pre>
<div class="block">Default constructor.</div>
</li>
</ul>
<a name="TypeConversionRule(mmj.verify.Grammar, mmj.lang.Axiom, mmj.lang.Cnst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>TypeConversionRule</h4>
<pre>public&nbsp;TypeConversionRule(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                  <a href="../../mmj/lang/Axiom.html" title="class in mmj.lang">Axiom</a>&nbsp;baseSyntaxAxiom,
                  <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;convTyp)</pre>
<div class="block">Constructor -- default GrammarRule for base Syntax Axioms, which means no
 parameter "transformations".</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar.</dd><dd><code>baseSyntaxAxiom</code> - Syntax Axiom.</dd><dd><code>convTyp</code> - the "from" type code of this conversion</dd></dl>
</li>
</ul>
<a name="TypeConversionRule(mmj.verify.Grammar, mmj.verify.NotationRule, int, mmj.verify.NullsPermittedRule)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>TypeConversionRule</h4>
<pre>public&nbsp;TypeConversionRule(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                  <a href="../../mmj/verify/NotationRule.html" title="class in mmj.verify">NotationRule</a>&nbsp;oldNotationRule,
                  int&nbsp;matchIndex,
                  <a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify">NullsPermittedRule</a>&nbsp;nullsPermittedRule)</pre>
<div class="block">Builds a new TypeConversionRule using a Notation rule which is being
 "cloned" and modified by substituting the paramTransformationTree from a
 NullsPermittedRule for one of the existing rule's variable hypothesis
 paramTransformationTree nodes.
 <p>
 (That sounds hairy :)
 <p>
 Note that the output paramTransformationTree is built using a deep clone
 of the existing rule's paramTransformationTree but the substituting tree
 does not need cloning BECAUSE when the GrammaticalParser builds a
 ParseTree for an expression, *it* does a full cloning operation; this, of
 course assumes that once a GrammarRule is created and fully populated
 that it is never modified (changing the grammar means rebuilding it, in
 other words.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar.</dd><dd><code>oldNotationRule</code> - rule being "cloned".</dd><dd><code>matchIndex</code> - index to paramVarHypNode array indicating which VarHyp
            is being substituted.</dd><dd><code>nullsPermittedRule</code> - the modifying rule.</dd></dl>
</li>
</ul>
<a name="TypeConversionRule(mmj.verify.Grammar, mmj.verify.TypeConversionRule, int, mmj.verify.TypeConversionRule)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>TypeConversionRule</h4>
<pre>public&nbsp;TypeConversionRule(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                  <a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;oldTCRule,
                  int&nbsp;matchIndex,
                  <a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;typeConversionRule)</pre>
<div class="block">Builds a new TypeConversionRule using an existing TypeConversion rule
 which is being "cloned" and and modified by substituting the
 paramTransformationTree from another TypeConversionRule for one of the
 existing rule's variable hypothesis paramTransformationTree nodes.
 <p>
 Note that the output paramTransformationTree is built using a deep clone
 of the existing rule's paramTransformationTree but the substituting tree
 does not need cloning BECAUSE when the GrammaticalParser builds a
 ParseTree for an expression, *it* does a full cloning operation; this, of
 course assumes that once a GrammarRule is created and fully populated
 that it is never modified (changing the grammar means rebuilding it, in
 other words.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar.</dd><dd><code>oldTCRule</code> - rule being "cloned".</dd><dd><code>matchIndex</code> - index to paramVarHypNode array indicating which VarHyp
            is being substituted.</dd><dd><code>typeConversionRule</code> - the modifying rule.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="buildBaseRule(mmj.verify.Grammar, mmj.lang.Axiom, mmj.lang.ParseNodeHolder[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>buildBaseRule</h4>
<pre>protected static&nbsp;<a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;buildBaseRule(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                               <a href="../../mmj/lang/Axiom.html" title="class in mmj.lang">Axiom</a>&nbsp;baseSyntaxAxiom,
                               <a href="../../mmj/lang/ParseNodeHolder.html" title="class in mmj.lang">ParseNodeHolder</a>[]&nbsp;parseNodeHolderExpr)</pre>
<div class="block">Type Conversion Rule builder for base Syntax Axioms, which means no
 parameter "transformations".</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar.</dd><dd><code>baseSyntaxAxiom</code> - Syntax Axiom.</dd><dd><code>parseNodeHolderExpr</code> - Expression in parseNodeHolder array.</dd>
<dt><span class="strong">Returns:</span></dt><dd>new TypeConversionRule object.</dd></dl>
</li>
</ul>
<a name="isLoop(mmj.lang.Cnst, mmj.lang.Cnst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isLoop</h4>
<pre>public static&nbsp;boolean&nbsp;isLoop(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;fromTyp,
             <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;toTyp)</pre>
<div class="block">isLoop determines whether or not a new Type Conversion from/to pair of
 Type Codes create a "loop" -- meaning that "from" converts to "to" and
 "to" converts to "from", directly or indirectly.
 <p>
 isLoop relies on Cnst.convFromTypGRArray already being fully populated
 with all "from" Type Codes for the subject Cnst, including direct
 conversions and all indirect conversions; this puts the onus on
 TypeConversionRule.deriveAdditionalRules to figure out the complicated
 stuff.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>fromTyp</code> - the "from" converstion Type Code.</dd><dd><code>toTyp</code> - the "to" converstion Type Code.</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if it is a loop, else false.</dd></dl>
</li>
</ul>
<a name="getDupRule(mmj.verify.Grammar, mmj.lang.Cnst[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getDupRule</h4>
<pre>public&nbsp;<a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a>&nbsp;getDupRule(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                     <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]&nbsp;ruleFormatExprIn)</pre>
<div class="block">Return a duplicate of the input ruleFormatExpr if it exists, or return
 null.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/verify/GrammarRule.html#getDupRule(mmj.verify.Grammar, mmj.lang.Cnst[])">getDupRule</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar.</dd><dd><code>ruleFormatExprIn</code> - the expression to check.</dd>
<dt><span class="strong">Returns:</span></dt><dd>GrammarRule if duplicate found, or null.</dd></dl>
</li>
</ul>
<a name="addToGrammar(mmj.verify.Grammar, mmj.lang.Cnst[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addToGrammar</h4>
<pre>public&nbsp;void&nbsp;addToGrammar(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]&nbsp;ruleFormatExprIn)</pre>
<div class="block">Add Type Conversion rule format expression to the system "repository".</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/verify/GrammarRule.html#addToGrammar(mmj.verify.Grammar, mmj.lang.Cnst[])">addToGrammar</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar object (Mr Big).</dd><dd><code>ruleFormatExprIn</code> - the expression to add.</dd></dl>
</li>
</ul>
<a name="deriveAdditionalRules(mmj.verify.Grammar)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>deriveAdditionalRules</h4>
<pre>public&nbsp;void&nbsp;deriveAdditionalRules(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar)</pre>
<div class="block">deriveAdditionalRules based on the addition of a new GrammarRule to those
 already generated and accepted.
 <p>
 A PriorityQueue is used to store new derivedGrammarRules awaiting
 processing (dup checking, parse checking and possible addition to the
 Grammar data.) The Comparator orders derived rules based on MaxSeqNbr and
 ruleNbr so that low Metamath sequence number statements are added to the
 Grammar before higher sequenced statements. The existing rules are stored
 in separate repositories, which are scanned, as needed, when a new rule
 is added; the order that the repositories are scanned is irrelevant
 because the PriorityQueue controls update processing sequence.
 <p>
 Note also that a newly derived rule may generate other derived rules,
 which in turn trigger other derivations; this is a "feature" (as well as
 a scary opportunity for an infinite loop!) The benefit is that each pair
 of rules may be considered separately; when processing the pair there is
 no need to worry about other possible Type Conversion and Null Permitted
 Rules. For example, an "A" Type hypothesis in a Notation Rule may be the
 target of a "B to A" Type Conversion, but the fact that there is a
 "C to B" or "C to A" conversion can be ignored -- if the "B to A"
 conversion generates a variant rule of the original rule, then when
 *that* rule comes back through the PriorityQueue, the "C to B" rule will
 automatically come into play. This also means that a "B to A" conversion
 will combine with a "C to B" conversion to generate a "C to A" conversion
 -- eventually.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/verify/GrammarRule.html#deriveAdditionalRules(mmj.verify.Grammar)">deriveAdditionalRules</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar.</dd></dl>
</li>
</ul>
<a name="deriveRulesUsingNullsPermitted(mmj.verify.Grammar, mmj.verify.NullsPermittedRule)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>deriveRulesUsingNullsPermitted</h4>
<pre>protected&nbsp;void&nbsp;deriveRulesUsingNullsPermitted(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                                  <a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify">NullsPermittedRule</a>&nbsp;nullsPermittedRule)</pre>
<div class="block">Generates a NullsPermittedRule *if* the input NullsPermittedRule Type
 Code matches the Type Code of the TypeConversionRule's VarHyp.
 <p>
 Note: The form of a TypeConversionRule *expression* is exactly one
 variable whose Type Code differs from that of the rule's Type.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar.</dd><dd><code>nullsPermittedRule</code> - the modifying rule.</dd></dl>
</li>
</ul>
<a name="deriveRulesUsingTypeConversion(mmj.verify.Grammar, mmj.verify.TypeConversionRule)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>deriveRulesUsingTypeConversion</h4>
<pre>protected&nbsp;void&nbsp;deriveRulesUsingTypeConversion(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                                  <a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;typeConversionRule)</pre>
<div class="block">Generates a TypeConversionRule *if* the input TypeConversionRule Type
 Code matches the Type Code of this TypeConversionRule's VarHyp.
 <p>
 Note: The form of a TypeConversionRule *expression* is exactly one
 variable whose Type Code differs from that of the rule's Type.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - The Grammar.</dd><dd><code>typeConversionRule</code> - the modifying rule.</dd></dl>
</li>
</ul>
<a name="getConvTyp()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getConvTyp</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;getConvTyp()</pre>
<div class="block">Return convTyp, the "from" part of the Type conversion.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>convTyp, the "from" part of the Type conversion.</dd></dl>
</li>
</ul>
<a name="getForestRuleExpr()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>getForestRuleExpr</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]&nbsp;getForestRuleExpr()</pre>
<div class="block">Returns the ruleFormatExpr for the Type Conversion Rule by simulating
 retrieving it from the Grammar Rule Tree/Forest.
 <p>
 In reality, the ruleFormatExpr for a Type Conversion Rule is an length =
 1 symbol sequence = convTyp.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/verify/GrammarRule.html#getForestRuleExpr()">getForestRuleExpr</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>ruleFormatExpr for the Type Conversion Rule.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/SubstMapEntry.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/VerifyProofs.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/TypeConversionRule.html" target="_top">Frames</a></li>
<li><a href="TypeConversionRule.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
